$\forall$$T$:Type\{i\}, ${\it eq}$:EqDecider($T$), $d$:$a$:$T$ fp$\rightarrow$ Type\{i\}. non{-}void($d$) $\in$ $\mathbb{P}$\{i'\}